%% Keywords for the B method

\newcommand{\MACHINE}{\ensuremath{\textbf{MACHINE }}}

%\newcommand{\MACHINE}{\operatorname{\textbf{MACHINE }}} % COMANDO ORIGINAL
\newcommand{\REFINEMENT}{\operatorname{\mathbf{REFINEMENT }}}
\newcommand{\IMPLEMENTATION}{\ensuremath{\textbf{IMPLEMENTATION }}}
\newcommand{\REFINES}{\ensuremath{\textbf{REFINES }}}
\newcommand{\SEES}{\ensuremath{\textbf{SEES }}}
\newcommand{\INCLUDES}{\ensuremath{\textbf{INCLUDES }}}
\newcommand{\IMPORTS}{\ensuremath{\textbf{IMPORTS }}}
\newcommand{\SETS}{\ensuremath{\textbf{SETS }}}
\newcommand{\CONSTANTS}{\ensuremath{\textbf{CONSTANTS }}}
\newcommand{\PROPERTIES}{\ensuremath{\textbf{PROPERTIES }}}
\newcommand{\CONCRETE}{\ensuremath{\textbf{CONCRETE }}}
\newcommand{\VARIABLES}{\ensuremath{\textbf{VARIABLES }}}
\newcommand{\ASSERTIONS}{\ensuremath{\textbf{ASSERTIONS }}}
\newcommand{\CONCRETEVARIABLES}{\ensuremath{\textbf{CONCRETE\_VARIABLES }}}
\newcommand{\DEFINITIONS}{\ensuremath{\textbf{DEFINITIONS }}}
\newcommand{\VAR}{\ensuremath{\textbf{VAR }}}
\newcommand{\IN}{\ensuremath{\textbf{IN }}}
\newcommand{\INVARIANT}{\ensuremath{\textbf{INVARIANT }}}
\newcommand{\INITIALISATION}{\ensuremath{\textbf{INITIALISATION }}}
\newcommand{\OPERATIONS}{\ensuremath{\textbf{OPERATIONS }}}
\newcommand{\BEGIN}{\ensuremath{\textbf{BEGIN }}}
\newcommand{\END}{\ensuremath{\textbf{END }}}
\newcommand{\PRE}{\ensuremath{\textbf{PRE }}}
\newcommand{\IF}{\ensuremath{\textbf{IF }}}
\newcommand{\THEN}{\ensuremath{\textbf{THEN }}}
\newcommand{\ELSE}{\ensuremath{\textbf{ELSE }}}
\newcommand{\ELSIF}{\ensuremath{\textbf{ELSIF }}}
\newcommand{\ANY}{\ensuremath{\textbf{ANY }}}
\newcommand{\WHERE}{\ensuremath{\textbf{WHERE }}}
\newcommand{\CASE}{\ensuremath{\textbf{CASE }}}
\newcommand{\OF}{\ensuremath{\textbf{OF }}}
\newcommand{\EITHER}{\ensuremath{\textbf{EITHER }}}
\newcommand{\AND}{\ensuremath{\textbf{AND }}}
\newcommand{\OR}{\ensuremath{\textbf{OR }}}
\newcommand{\NOT}{\ensuremath{\textbf{NOT }}}
\newcommand{\WHILE}{\ensuremath{\textbf{WHILE }}}
\newcommand{\DO}{\ensuremath{\textbf{DO }}}
\newcommand{\VARIANT}{\ensuremath{\textbf{VARIANT }}}
\newcommand{\FALSE}{\ensuremath{\textbf{FALSE }}}
\newcommand{\TRUE}{\ensuremath{\textbf{TRUE }}}

%% Commonly used math entities
\newcommand{\pow}{\ensuremath{\textbb{P }}}
\newcommand{\nat}{\ensuremath{\textbb{N }}}
\newcommand{\pfun}{\ensuremath{\rightarrow\mkern-22mu+}}
\newcommand{\fset}{\ensuremath{\textbb{F }}}
\newcommand{\dom}{\ensuremath{\mbox{dom}}}
\newcommand{\ran}{\ensuremath{\mbox{ran}}}
\newcommand{\natone}{\ensuremath{\textbb{N}_1}}
\newcommand{\integer}{\ensuremath{\textbb{Z }}}
%\newcommand{\fun}{\ensuremath{\rightarrow}}
\newcommand{\domr}{\ensuremath{\triangleleft}}
\newcommand{\seq}{\ensuremath{\textbf{seq1 }}}
\newcommand{\ovr}{\ensuremath{\oplus}}
\newcommand{\BOOL}{\ensuremath{\textbf{BOOL }}}
\newcommand{\pred}{\ensuremath{\textbf{pred }}}
\newcommand{\Bsucc}{\ensuremath{\textbf{succ }}}

